Thanks for this PR and the detailed documentation both @OskarSoderberg and @woosh !

get-2.c
The predicate generation error can happen when the theory of heaps is present, this is something we are currently working on improving.

The following version, although it contains undefined behavior, leads to a solution:

int get(int* p) {
    if (*p <= 0) {
        return 0;
    } else {
        *p = *p - 1;
        return 1 + get(p);
    }
}

void main()
{
  //Non-det assignment of variables
  int *n, n_init, r1;
  assume((n_init > 0));

  n = (int*) malloc(sizeof(int));
  // *n = n_init;
  assume(*n == n_init);
  r1 = get(n);

  assert(((r1 >= n_init) && (r1 <= (n_init * n_init))));
}

incdec-3.c
Maybe there are some opportunities to optimize the solution post-processsors, currently they seems to take a long time even for relatively simple solutions. The error might be related.

max-1: The requires clause was
requires x == a && y == b && \separated(x, y) && \valid(x) && \valid(y);
but now what gets generated is
requires x == a && y == b;

I think this one is a bug; but before coming to that, it is also good to know that TriCera now does not check for memory safety properties by default since PR #10. To check the same properties prior to this PR, the options -reachsafety -valid-deref -valid-free can be passed.

Having said that, the issue in this benchmark does not seem to be related to that. I couldn't spend enough time to fully debug this yet, but the visitor here is likely the culprit. I think it operated on some assumptions which are no longer there. In this benchmark the solution contains two existential quantifiers, and after this visitor the formula is no longer well-formed -- the quantifiers are still there and the De Brujin indexes of the arguments are shifted. I am not yet sure how to fix this, but it seems to me that without at least the valid predicates the precondition becomes too weak.

I think we can land the PR without fixing above bug after a few changes, let me know if you want to hold on until fixing the bug.

@woosh Please let me know when you want to land this, from my side it is good to go after only disabling the translation of solutions with -log. The postcondition simplification can be optimized but this is probably not very urgent.

Maybe we should hold this PR just for a little. I have been looking into the "missing" \separated(...) and \valid(...) terms in the inferred contract for e.g. max-1.c. Adding the options -reachsafety -valid-deref -valid-free didn't make any difference. However, Oscar had a branch in his repository called theory-of-heaps-translation-thesis-version containing a few changes, mainly to the ADTExploder.

I have rebased those changes on the branch for this PR, (see patch). To be honest I have not fully grasped why, but these changes made the terms appear in the contracts again.

However, while working with that I ran into another issue. I get inconsistent results for e.g. get-1.c. Occasionally I get a contract for this case, but sometimes I get Out of memory and most often it just times out. Working together with @gustavung we managed to narrow down the problem to a fix-point iteration in EqualitySwapper when processing the post condition. There it ends up in a situation where it is alternating between two different expressions.

We can still land this PR and make a new one for the iterator fix. But I'm not 100% sure that the regression tests for this PR will always work at the moment because of the above mentioned inconsistent results.

Question: If we merge this PR, should I first push the fix for the \sepratated(...) and \valid(...) terms.

I have rebased those changes on the branch for this PR, (see patch). To be honest I have not fully grasped why, but these changes made the terms appear in the contracts again.

Great! I think the fix is due to the line replacing emptyHeap with a fresh heap term at program entry. This adds a quantified heap term to the solutions, replacing the emptyHeap as the initial term, which the methods here seem to depend on to build a mapping.

I think there are two issues here, which I believe are separate:

• the building of the heap map used for inferring valid and separated predicates
• starting the program with a fresh heap term rather than the empty heap.

The former not working with an empty starting heap seems like a bug to me, it should be possible to build this map regardless of the initial value of the heap.

Starting the program with a fresh heap term makes sense when the entry point to the program is not main, but otherwise starting with an emptyHeap seems like the correct semantics to me? @pruemmer, any thoughts on this? If that makes sense, we could use a fresh heap term (as in the patch you linked) when an entry other than main is explicitly specified using the CLI, and otherwise default to the emptyHeap.

This would break the building of the heap map again in max-1.c and other examples . We could also add an option to switch the starting heap mainly so that this functionality works for now, but ideally the heap map building should work in both cases.

However, while working with that I ran into another issue. I get inconsistent results for e.g. get-1.c. Occasionally I get a contract for this case, but sometimes I get Out of memory and most often it just times out. Working together with @gustavung we managed to narrow down the problem to a fix-point iteration in EqualitySwapper when processing the post condition. There it ends up in a situation where it is alternating between two different expressions.

I think the postcondition simplifier can be optimized, but this requires some more thought and work to get right. Since this is an issue only with -acsl (after we disable this functionality when using -log), I propose leaving that work for another PR, and disabling the unstable regression tests for now. Creating an issue for the unstable tests sounds good to me!

@zafer-esen I think this PR is ready for merge. The commit ed405fe is a fix for using an empty heap instead of a quantified heap term when doing contract translation.

Trying to use a quantified heap term breaks other regression test suits, like horn-hcc-heap, horn-hcc-array, acsl-contracts, uninterpreted-predicates, with errors

java.lang.Exception: Predicate generation failed
(error "Predicate generation failed")
Other Error: Predicate generation failed

(error "assertion failed")
java.lang.AssertionError: assertion failed
Other Error: assertion failed

I think being able to start with an arbitrary entry function and a fresh heap term would be a nice extension, but I consider that future work.

I have also disabled test cases in toh-contract-translation/runtests that are currently known to fail. These are

get-2      (predicate generation failure)
incdec-3   (out of memory)
multadd-2  (out of memory)
multadd-3  (timeout)
truck-1    (out of memory)

I have created separate issues describing the reasons for disabling them, please see #15, #16, #17

Thanks for a quick merge 😃 Would it be possible to create a new release at this point?

Sure, I am trying to fit in a few more features and fix a few more bugs, will do a release this week!